| Definitions | (e <loc e'), e c e', e loc e' , sender(e), s ~ t, A List , n+m, -n, Outcome, False, i  j , A B, first(e), pred(e), pred!(e;e'), kind(e), loc(e), SWellFounded(R(x;y)),  x:A. B(x), (x  l), n - m, #$n, {T}, a < b, constant_function(f;A;B), r s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  ,  , Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ),   x. t(x), Knd, EState(T), EOrderAxioms(E; pred?; info), Id, IdLnk, EqDecider(T), x.A(x),  T, Unit,  , p   q, p  q, p   q, e = e', deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, x f y, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, True, f(x)?z, type List, P  Q, P & Q, P Q, {x:A| B(x)} ,  x:A.B(x), Void, Top, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), x dom(f), strong-subtype(A;B), x,y. t(x;y), as @ bs, [car / cdr], [], X(e), E(X), a:A fp B(a), tt,  b, e X, prior(X), ff, (e < e'), prior-state(f;base;X;e), list_accum(x,a.f(x;a);y;l), f(a), es-prior-interface-vals(es;X;e), t.1, let x,y = A in B(x;y), left + right,  b, x:A  B(x),  , P Q,  , <a, b>, AbsInterface(A), Type, ES, s = t, t T, A,  x:A. B(x), E, x:A B(x) |